//package br.cin.ufpe.rabbit;
//
//import gov.nasa.jpf.jvm.FieldInfo;
//import gov.nasa.jpf.jvm.ThreadInfo;
//import gov.nasa.jpf.jvm.bytecode.Instruction;
//import java.util.Map;
//import java.util.Set;
//
//class MemAccess {
//	Instruction insn;
//	ThreadInfo ti;
//	LockSet ls;
//
//	boolean isSymetric(MemAccess another) {
//		if (insn.equals(another.insn) && this.ls.equals(another.ls)
//				&& !ti.equals(another.ti)) {
//			return true;
//		}
//		return false;
//	}
//}
//
//class PotRaceInfo {
//	Object objRef;
//	FieldInfo fi;
//	MemAccess ma1, ma2;
//}
//
//public class mock {
//	Map<Integer, Map<FieldInfo, Set<MemAccess>>> rwset;
//
//	void executeInstruction(Instruction insn){ 
//
//	  if(!insn.isFieldInstruction()) return;
//
//	  ThreadInfo ti = getCurrentThread();
//	  // peek the object reference from stack
//	  int objRef = ti.peek();             
//	  FieldInfo fi = insn.getFieldInfo();
//	  LockSet ls = ti.getLockSet()
//
//	  MemAccess memAccess = new MemAccess(insn, ti, ls);
//
//	  checkRace(objRef, fi, memAccess);   
//
//	  updateRWSet(rwset, objRef, fi, memAccess);
//	  
//	}
//
//	void checkRace(Integer objRef, FieldInfo fi, MemAccess ma1){
//
//	  Set<PotRaceInfo> potentialRaces;
//	  
//	  // pass 1: find conflicts
//	  foreach(ma2 in rwset.get(objRef).get(fi)){
//	    if (isRead(currAccess.insn) && isRead(memAccess.insn) {
//	      continue;
//	    }
//	    if (intersect(currAccess.ls, memAccess.ls).isEmpty()) {
//	      PotRaceInfo potRace =
//	        new PotRaceInfo(objRef, fi, currAccess, ma2);
//	      potentialRaces.add(potRace);
//	    }
//	  }
//	  
//	  Set<PotRaceInfo> filteredPotencialRaces;
//	  foreach(potRace in potencialRaces){
//	    if(!potRace.ma1.isSymetric(potRace.ma2)){
//	    	filteredPotencialRaces.add(potRace);	
//	    }
//	  }
//
//	  // pass 3: find simple causalities
//	}
//}
